{-# OPTIONS -XBangPatterns -fglasgow-exts -funbox-strict-fields -O2 -optc-O3 #-}
module Main where 

import System.Environment (getArgs)

import Data.Map
import Data.List
import Data.IORef
import Data.Maybe
import Numeric

import Monad
import Control.Monad
import Control.Exception
import Control.Monad.State 

import Debug.Trace

import Engine
import EngineTypes
import Compiler
import IO
import RPTypes
import SParser hiding (mtrace)
import AtomMap
import HistTree hiding (findWithDefault)
import TableAccounting hiding (updateWeights)
import Query hiding (mtrace)

main :: IO ()

main =
    do args <- getArgs
       if (length args) /= 1
          then hterminate
          else rp4 (head args)
{-
main = do args <- getArgs
          if (length args) /= 2
             then hterminate
             else let [query,program] = args
		      in case query of
			     "krk" -> rp4 program (head krk_ded) (head krk_ind)
			     "mst" -> rp4 program (head mst_ded) (head mst_ind)
			     -- "divn2" -> rp4 program divn_ded divn_ind
			     otherwise -> putStrLn "Query complied in; see Main.hs"
-}

-- main = nqtest (head (mtrace ( stringToCBody (mtrace ))))
{-
main = let (a,d,i) = phase3 $ phase2b $ phase2a $ fst $ phase2 $ phase1 $ head $stringToCBody (testString3)
       in do print ("All is: " ++ (show a) )
             print ("Ded is: " ++ (show d))
             print ("Ind is: " ++ (show i))

testString1 = "rnot (q(Z), rnot rnot (r ; rnot p(X,Y)))"
testString2 = "rnot (forall ~ X ::: exists ~ Y ::: p(X,Y))"

testString3 = "rnot (forall ~ X ::: exists ~ Y ::: q(X),p(X,Y))"
-}
-- main = print $ phase2 $ phase1 $ head $stringToCBody (mtrace "(q(X), r(X))")

-- main = print $ phase2b $ phase2a $ fst $ phase2 $ phase1 $ head $ stringToCBody (mtrace "rnot rnot ( rnot p(X,Y,Z)), q(X)")

-- Keep these around for Hugs debugging

-- main = prolog "test12.rp" inout
-- main = prolog "mst.rp" (head msttest4)
-- main = rp4 "divn2.rp" divn_ded divn_ind
-- main = rp4 "mst_r.rp" (head mst_ded) (head mst_ind)
-- main = prolog "test10.rp" (CTERM (dLL nthtest2))
-- main = parseTest "test10.rp"
-- main = rp4 "krk5.rp" (head krk_ded) (head krk_ind)
-- main = prolog "krk5.rp" (head krk_ded)

hterminate = do putStrLn "Command line help in here"; return ()

{-
main = putStrLn ("Test : " ++ (show (compileTerm tt vmap)))
    where vmap = varMap (CLA tt CNIL)
          tt = dLL nthtest
-}

ttt (CTERM x _) = x

prolog:: String -> CBody -> IO ()
prolog str query =  
    do if debug then putStr "About to run\n" else return ()
       ints <- internalClauses
       parsedata <- fileToClauses str
       result <- (wamExecProlog query (ints ++ parsedata))
       putStr result
       return ()

wamExecProlog :: CBody -> [Clause] -> IO String
wamExecProlog t c = (cc t c)

parseTest:: String -> IO ()
parseTest str =  
    do putStr "PARSE TEST\n"
       ints <- internalClauses
       parsedata <- fileToClauses str
       putStr (show parsedata)
       return ()

rp4 :: String -> IO ()
rp4 filename =
    do hSetBuffering stdin NoBuffering
       if debug then putStrLn ("About to read: " ++ filename)  else return ()
       ints <- internalClauses
       parsedata <- fileToClauses filename
       if debug then putStrLn "Parse finished" else return ()
       result <- (wamExecRP4 (ints ++ parsedata))
       putStr result

wamExecRP4 :: [Clause] -> IO String
wamExecRP4 c = (ccRP c)

internalClauses :: IO [Clause]
internalClauses = fileToClauses name
    where name = "tests\\internals.rp"

cc :: CBody -> [Clause] -> IO String
cc t c = do wd <- compileSetup
            compileProgram wd c
            dd "Program Compile done, compiling query ...\n"
            (start,regids) <- compileQuery wd t
            str <- dumpCode wd
            dd str
            dd ("Start is " ++ (show start) ++ "\n") 
            setPC wd start
            prologExec wd 
            
prologExec wd  =
         do execCode wd
            res <- callRandList wd
            ddout ("Clist is: " ++ (show res) ++ "\n")
            qres <- getQueryResult wd
            if qres == True
               then do ddout "Answer found; huzzah!\n"
                       hSetBuffering stdout NoBuffering
                       c <- if not alwaysContinue 
                               then do ddout "continue? (y/n)"
                                       ch <- getLine
                                       hSetBuffering stdout LineBuffering
                                       return ch
                               else return "dummy"
                       if alwaysContinue || (((length c) > 0) && (head c) == 'y') 
                          then do doWAMFail wd -- backtrack on inductive phase
				  -- ADD A TRUST HERE
                                  incPC wd -- inc PC outside of engine
                                  prologExec wd -- somehow continue the computation
                          else return []
               else do ddout "No answer found.\n"
                       return []

ccRP :: [Clause] -> IO String
ccRP c = 
    do (wd,dref,iref,hp,pregs,printregs) <- compileRP c
       -- str <- dumpCode wd
       -- ddout str
       if debug then putStrLn "Compile finished" else return ()
       printRunInfo wd
       execRP wd dref iref hp pregs printregs
       dd "All done\n"
       return []

compileRP :: [Clause] -> IO (WAMData a, WAMRef,WAMRef,WAMRef,Arity,[(Variable,Register)])
compileRP prog = 
           do wd <- compileSetup
              compileProgram wd prog
              (ded,ind) <- getCompiledQuery wd
              -- pushCode wd (Allocate (length (permRegs varmap)))
              doq wd ded ind
              where doq wd ded ind =     
                        let  varmap = (varMap (CLA (T "a" 0 [] nullpos) (CCONJ ded ind Notset)))
                             dedvars = [ v | (v,x) <- assocs $ varCounts ded ]
                             dedregs = [ (v,findWithDefault NullRegister v varmap) | (V v _) <- dedvars ]
                        in do resetRegister wd 
                              startded <- compileQueryV wd ded varmap
                              pushCode wd HaltOP
                              startind <- compileQueryV wd ind varmap
                              haltpoint <- pushCode wd HaltOP
                              dd ("Startded is " ++ (show startded) ++ " startind is " ++ (show startind) ++ "\n")
                              if debug 
	                       then do str <- dumpCode wd
                                       dd str
	                       else return ()
                              return (wd,startded,startind,haltpoint,(fromIntegral $ length $permRegs varmap), dedregs)

execRP :: (WAMData a) -> WAMRef -> WAMRef -> WAMRef -> Arity -> [(Variable,Register)] -> IO ()
execRP wd sd si haltpoint pregs  registers = 
           do cix <- readIORef $ clauseIDIndex wd
	      -- execCodeEntryInst wd (fst (wAMOpToWAMOpRaw (Allocate pregs) cix))
	      allocate pregs wd
              regaddrs <- mapM rm (Data.List.map (\(x,y) -> (x,registerToRaw y)) registers)
	      ct <- getCT wd
	      setOCT wd ct
              setPC wd sd
              try_here 5 haltpoint (exceptCID wd) wd -- push the deductive exception choice point here
	      -- dh wd
	      -- ddout ("START DUMP DONE\n")
              bp <- getBP wd
              setDedBP wd bp
	      setChoiceBottom wd bp
              zeroDeductiveCount wd 
              setQueryResult wd True
              execRPDed wd si sd haltpoint regaddrs
           where rm (x,y) = do reg <- regmap wd y
                               return (x,reg)

printSols wd regids =
    do mapM (printThing) regids
       return ()
    where printThing (v,r) = do ddout (v ++ " = ")
                                printAddr wd r

witnessSize wd regids =
    do vals <- mapM (ws) regids
       return (sum vals)
    where ws (_,r) = termSize wd r

retry_reset wd haltpoint =
    do doWAMFail wd -- sets B0P and pc to next
       bp <- getBP wd
       popCallStackBPINC wd bp
       retry_here haltpoint (exceptCID wd) wd
       newct <- getHEntry wd (bp + oOldCodeTop)
       setCT wd (deref1 newct)
       -- ddout ("RESETTING FOR DEDUCTIVE PHASE DONE; NEW BP IS: " ++ (show bp) ++ " NEW CT IS: " ++ (show (deref1 newct)) ++ "\n")
       return ()

execRPDed wd si sd haltpoint regids = 
    do reset <- updateRestartThreshold wd
       if reset
          then do dedbp <- getDedBP wd
                  setBP wd dedbp
		  retry_reset wd haltpoint
		  setQueryResult wd True
		  setPC wd sd
                  zeroDeductiveCount wd 
                  ddout "RESETTING\n"
		  pT wd
		  return ()
	  else return()
       execCode wd
       qresd <- getQueryResult wd
       callgraph <- callRandList wd
       inst_count <- getGlobalCount (cInstCount wd)
       -- ddout ("DEDUCTIVE: Query result is " ++ (show qresd) ++ " inst count is: " ++ (show inst_count) ++ " instCountMax is: " ++ (show instCountMax) ++ "\n")
       if qresd && inst_count < instCountMax
	  then do cg <- callList wd
		  dd ("about to attind callgraph is " ++ (show cg) ++ "\n")
                  dd ("brief cg is: " ++ (show callgraph) ++ "\n")
		  rt <- readIORef $ randTable wd
		  if isNothing $ lookupM callgraph rt
                     then do if printPossibleWitnesses
				then do rth <- readIORef (EngineTypes.restartThreshold wd)
					pch <- readIORef $pointChange wd
					inst_count <- getInductiveCount (cInstCount wd) 
					ddout ("Current (restart) count is " ++ (show inst_count) ++ " thresh: " ++ (show rth) ++ " pointChange: " ++ (show pch) ++ "\n")
					ddout "Possible witness: "
					printSols wd regids
					return ()
				else return ()
			     attemptInd wd callgraph si sd haltpoint regids
		     else do if printPossibleWitnesses 
				then ddout "." 
				else return ()
                             dedReset wd callgraph si sd haltpoint regids
	  else do ddout "Initial query fails\n"
		  return ()

updateRestartThreshold :: (WAMData a) -> IO Bool
updateRestartThreshold wd =
     do pointCH <- readIORef $ pointChange wd
	rth <- readIORef (EngineTypes.restartThreshold wd)
        inst_count <- getDeductiveCount (cInstCount wd)
	st <- readIORef $ shortThreshold wd
	case pointCH of
	  1  -> do if inst_count > rth 
		      then do writeIORef (EngineTypes.restartThreshold wd) st  -- restartThresholdDefault for long and short here
			      writeIORef (pointChange wd) 0
			      writeIORef (origChange wd) (nullCID wd)
			      return True
		      else return False
	  0 -> do if inst_count > rth -- && rth > minimumRestartThreshold
		     then do writeIORef (EngineTypes.restartThreshold wd) st
			     writeIORef (pointChange wd) pointChangeDefault	
			     writeIORef (origChange wd) (nullCID wd)
			     return True
		     else {- if rth < minimumRestartThreshold
		             then do writeIORef (EngineTypes.restartThreshold wd) minimumRestartThreshold 
			     else -} return False
	  otherwise -> do if inst_count > rth 
			      then do writeIORef (EngineTypes.restartThreshold wd) st
				      writeIORef (pointChange wd) (pointCH - 1)
				      writeIORef (origChange wd) (nullCID wd)
				      return True
			      else return False

mtrace x = (trace ("MTRACE: " ++ (show x)) x)

printCG  = False
alwaysFail =True

attemptInd wd callgraph si sd haltpoint regids = 
     do dd ("Attempting inductive phase at " ++ (show si) ++ "\n")
        -- push ExceptCID CP here ...
	witsize <- witnessSize wd regids
	if printPossibleWitnesses && printCG then ddout ("Witness Size is " ++ (show witsize) ++ "\n") else return ()
	pc <- getPC wd  -- this will be the PC from the deductive phase; the HALTOP
	try_here 5 si (exceptCID wd) wd
	oldcb <- getChoiceBottom wd
	bp <- getBP wd
	setChoiceBottom wd bp
	setPC wd si -- set the PC to the start of the inductive phase
		    --
	zeroInductiveCount wd 
	-- +++++ AND EXECUTE
        trialCount <- (readIORef $ indTrialCount wd)
        (solution,trials) <- execRPInd wd False 0 trialCount
	-- +++++
	(calls,insts) <- getCounts wd inductiveCount
	multiple <- readIORef $ weightMultiple wd
	cix <-  readIORef $ clauseIDIndex wd
	if printPossibleWitnesses 
	   then do ddout ("Weight update; val: " ++ (showFFloat (Just 2) (instWeight (insts*(fromIntegral multiple)) witsize trials) "") ++ " calls: " ++ (show calls) ++ " insts: " ++ (show insts) ++ " trials: " ++ (show trials))
		   if printCG then  ddout (" mutiplier " ++ (show multiple) ++ " callgraph: " ++ (show (Data.List.map (\x -> fromJust$ AtomMap.lookupAtom x cix) callgraph)) ++ "\n")
		      else ddout "\n"
	   else return ()
	updateWeights wd (RTE(callgraph,1,(instWeight (insts*(fromIntegral multiple)) witsize trials)))
	setBP wd bp
	setChoiceBottom wd oldcb
	-- popCallStackBPNINC wd bp -- pop the gumph created in the exec
	doWAMFail wd
	trust_here (exceptCID wd) wd -- this should restore state up to the last inductive phase
	popCallStackNull wd -- pop the except
	if not solution
	   then do ddout "Answer found; huzzah!\n"
		   printSols wd regids
		   hSetBuffering stdout NoBuffering
		   c <- if not (alwaysContinue || alwaysFail)
			   then do ddout "continue? (y/n)"
				   ch <- getLine
				   hSetBuffering stdout LineBuffering
				   return ch
			   else return "dummy"
		   if not alwaysFail || (alwaysContinue || (((length c) > 1) && (head c) == 'y') )
		      then do setQueryResult wd True
			      doWAMFail wd -- backtrack on inductive phase
			      incPC wd -- inc PC outside of engine
			      execRPDed wd si sd haltpoint regids -- somehow continue the computation
		      else return ()
	   else dedReset wd callgraph si sd haltpoint regids
			 
dedReset wd callgraph si sd haltpoint regids = 
                                         do if printPossibleWitnesses && printCG then ddout "BACKTRACK ON INDUCTIVE\n" else return ()
					    setQueryResult wd True
					    doWAMFail wd 
					    tc <- readIORef (currTrialCount wd) 
					    -- ddout ("TC is: " ++ (show tc) ++ "\n")
					    if tc == 0
				    	       then do -- ddout "TRIAL COUNT RESET\n"
				    	               incPC wd -- we must Inc the PC if we fail outside execcode
				    	               writeIORef (currTrialCount wd) trialCount
				    		       execRPDed wd si sd haltpoint regids
				    	       else do writeIORef (currTrialCount wd) (tc - 1)
				    		       attemptInd wd callgraph si sd haltpoint regids 

execRPInd wd solved trials trialsleft = 
                      do -- ddout "About to ind exec\n"
                         execCode wd
                         -- ddout "Ind exec done\n"
                         qresi <- getQueryResult wd
                         if qresi -- inductive succeeds
                            then do dd "Inductive Solution; about to fail\n"
				    if allSolutions && trialsleft > 0  --- trialsleft only applies if allsols is on
				       then do setQueryResult wd True
					       doWAMFail wd -- backtrack on inductive phase
					       incPC wd -- inc PC outside of engine
					       execRPInd wd True (trials + 1) (trialsleft - 1)-- look for more solutions to fill in the graph
				       else return (True,trials + 1)
                            else return (solved,trials + 1)


pT :: (WAMData a) -> IO ()
pT wd = do
     pointCH <- readIORef $ pointChange wd
     if printTree && (pointCH == 0)
	then do ht <- readIORef $ randTable wd
		cix <- readIORef $ clauseIDIndex wd
		ddout $ HistTree.showTreeParts nprint (cidprint cix) treeDepth $ getRT ht
	else return ()
     where cidprint ix ref = show $ fromJust $ AtomMap.lookupAtom ref ix


printRunInfo wd = 
    do rt <- readIORef $ randTable wd
       srt <- readIORef $ shortThreshold wd
       seed <- readIORef $ seed wd
       let lambda = getLambda rt
	   scale = getScale rt
	   in ddout ("RP4 - Scale is: " ++ (show scale) ++ " lambda is: " ++ (show lambda) ++ " shortTheshold is: " ++ (show srt) ++ " seed is: " ++ (show seed) ++"\n")



instWeight :: (Integral a, Integral b, Integral c) => a -> b -> c -> Double
-- instWeight i s t = ((fromIntegral i)**3)/((fromIntegral s)*(fromIntegral t)*(1000)**3)
instWeight i s t = 10000/(fromIntegral t)

{- The following are for little tests -}

{-

testcla1 = (CLA (T "f" 3 [(T "argx1" 1 [(V "X")]),(T "argf" 1 [(T "argx2" 1 [(V "X")])]),(T "noarg" 0 [])]) CNIL)
testcla2 = (CLA (T "f" 3 [(V "X"),(V "X"),(T "a" 0 [])]) CNIL)
testcla3 = (CLA (T "f" 3 [(T "a2" 2 [(V "Z"),(T "b" 0 [])]),
                          (V "W"),
                          (T "a2" 2 [(T "a" 0 []),(V "W")] ) ] )
                CNIL)
testterm = (T "f" 3 [(V "X"),(V "Y"),(V "X")])

testcla4 = (CLA (T "f" 1 [(T "g" 2  [(V "X"),(V "X")] )]) CNIL)

testterm2 = (T "f" 1 [(T "g" 2  [(T "a" 0 []),(V "Y")])] )

-- to go with test4.rp
testterm3 = (T "fla" 1 [(V "X")])

neqtest1 = (T "\\=" 2 [(T "a" 0 []),(T "a" 0 [])])
neqtest2 = (T "\\=" 2 [(T "a" 0 []),(T "b" 0 [])])
neqtest3 = (T "\\=" 2 [(stringToTerm "f(X,X,X)"),(stringToTerm "f(a,Y,a)")]) -- DOES NOT WORK HERE

tc1 = (CLA (T "f" 1 [(T "a" 0 [])]) CNIL)
tt1 = (V "X")
tt2 = (T "f3" 3 [(V "X"),(T "f2" 2 [(V "X"),(V "Y")]),(T "f1" 1 [(T "a" 0 [])])])
 
simpterm = (T "a" 0 [])

simpterm2 = (T "r" 0 [])
simpterm3 = (T "u" 0 [])
simpterm4 = stringToCBody "p;q;r"

-- for divn

dt1 = stringToTerm "plus(s(0),s(0),X)"
dt2 = stringToTerm "neg_mod(s(s(s(s(s(s(0)))))),s(s(0)),0)"

divn_ded = CTERM (T "numeral" 1 [(V "X")])
divn_ind = CCONJ (CTERM (T "$evidencediv2" 1 [(V "Y")])) (CTERM (T "neg_mod" 3 [(V "Y"),(V "X"),(T "0" 0 [])]))
divn_ind2 = CTERM (stringToTerm "p(X)")

-}
 
nthtest = stringToTerm "nth(0,[H|_],H)"
nthtest2 = stringToTerm "nth(6,[a,b,c,d,e],E)"

inout = head $ stringToCBody "inout(X),print(X)"

uniqtest =  stringToCBody "uniq([a,a,a],X),print(X)"

msttest = stringToCBody "G = graph([n1,n2,n3,n4],[v(n1,n3,1),v(n1,n4,2),v(n1,n2,3),v(n2,n3,7)]), T = subgraph([in,in,in,in]), edgeof(E,G),  print(checking),print(E),((edgeofsg(E,T,G), not_kruskal_invariant(E,T,G)); (not_edgeofsg(E,T,G), kruskal_invariant(E,T,G)))"
msttest2 = stringToCBody "G = graph([n1,n2,n3,n4],[v(n1,n3,1),v(n1,n4,2),v(n1,n2,3),v(n2,n3,7)]), T = subgraph([out,out,out,out]), edgeof(E,G), ((edgeofsg(E,T,G), print(E));(not_edgeofsg(E,T,G), print(not), print(E)))"
msttest3 = stringToCBody "G = graph([n1,n2,n3],[v(n1,n3,1),v(n1,n2,3),v(n2,n3,7)]), T = subgraph([in,out,in]), cyclic(G,T)"
msttest4 = stringToCBody "subset(X,15),print(X)"


mst_ded = stringToCBody "orderedgraph(G) , subgraph(G,T)"
mst_ind = stringToCBody "(edgeof(E,G),((edgeofsg(E,T,G),not_kruskal_invariant(E,T,G));(not_edgeofsg(E,T,G),kruskal_invariant(E,T,G))))"
-- mst_ind = 

krk_ded = stringToCBody "hypothesis(X)"
-- krk_ind = stringToCBody "(`illegal(Y1),print(Y1),unsatisfied(X,Y1));(`not_illegal(Y2),print(Y2),satisfied(X,Y2))"
-- krk_ind = stringToCBody "(`not_illegal(Y1),satisfied(X,Y1));(`illegal(Y2),print(Y2),unsatisfied(X,Y2))"
krk_ind = stringToCBody "check(X,Y)"
-- krk_ind = stringToCBody "repeat10,check(X,Y)"
